-- Previously Agda accepted invalid module names when no module header
-- was given.
